Termination proof of /tmp/tmpHdpftn/Ex4

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The replacement map contains the following entries:

f: {1}
cons: {1}
g: {1}
0: empty set
s: {1}
sel: {1, 2}

↳ CSR

  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The replacement map contains the following entries:

f: {1}
cons: {1}
g: {1}
0: empty set
s: {1}
sel: {1, 2}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The replacement map contains the following entries:

f: {1}
cons: {1}
g: {1}
0: empty set
s: {1}
sel: {1, 2}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g, s, sel, G, SEL, F} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

G(s(X)) → G(X)
SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The collapsing dependency pairs are DP_c:

SEL(s(X), cons(Y, Z)) → Z

The hidden terms of R are:

f(g(X))
g(X)

Every hiding context is built from:

g on positions {1}
f on positions {1}

Hence, the new unhiding pairs DP_u are :

SEL(s(X), cons(Y, Z)) → U(Z)
U(g(x_0)) → U(x_0)
U(f(x_0)) → U(x_0)
U(f(g(X))) → F(g(X))
U(g(X)) → G(X)

The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 3 less nodes.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g, s, sel, G} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:

G(s(X)) → G(X)

The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

G(s(X)) → G(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
G(x1) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g, s, sel} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g, s, sel} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(g(x_0)) → U(x_0)
U(f(x_0)) → U(x_0)

The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(g(x_0)) → U(x_0)
U(f(x_0)) → U(x_0)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, g, s, sel, SEL} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The TRS R consists of the following rules:

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SEL(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

f(X) → cons(X, f(g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

f(x0)
g(0)
g(s(x0))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.